package kodkod.analysis;

import kodkod.analysis.AST.ExtendedVoidVisitor;
import java.util.*;
import kodkod.ast.*;
import kodkod.ast.operator.FormulaOperator;

public class DeclVisitor extends ExtendedVoidVisitor {
	
	Analyzer analyzer;
	
	boolean negated = false;
	
	LinkedList<Integer> orwidth = new LinkedList<Integer>();
	boolean isolate = true;
	
	public DeclVisitor(Analyzer analyzer) {
		this.analyzer = analyzer;
	}
	
//	public void visit(NotFormula not) {
//		negated = !negated;
//		super.visit(not);
//		negated = !negated;
//	}
//	
//	public void visit(NaryFormula node) {
//		if (negated == node.op().equals(FormulaOperator.AND)) {
//			if (isolate) {
//				orwidth.add(orwidth.getLast() + node.size());
//				isolate = false;
//			} else {
//				int newwidth = orwidth.removeLast() + node.size();
//				orwidth.add(newwidth);
//			}
//		}
//		super.visit(node);
//	}
//
//	@Override
//	public void visit(BinaryFormula node) {
//		if ((negated && node.op().equals(FormulaOperator.AND)) || (!negated && node.op().equals(FormulaOperator.OR))) {
//			orDepth++;
//			node.left().accept(this);
//			node.left().accept(this);
//			orDepth--;
//		} else if (node.op().equals(FormulaOperator.IMPLIES)) {
//			orDepth++;
//			negated = !negated;
//			node.left().accept(this);
//			negated = !negated;
//			node.right().accept(this);
//			orDepth--;
//		} else {
//			if (NEGATION_DOUBLE_VISIT) orDepth++;
//			super.visit(node);
//			if (NEGATION_DOUBLE_VISIT) {
//				negated = !negated;
//				super.visit(node);
//				negated = !negated;
//			}
//			if (NEGATION_DOUBLE_VISIT) orDepth--;
//		}
//	}
	
	public boolean visited(Node node) {return false;}
	@Override
	public void visit(Decl decl) {
		super.visit(decl);
		analyzer.decls.put(decl.variable(), decl.expression());
	}
	@Override
	public void visit(Relation relation) {
		if (Analyzer.translation.primaryRelations.contains(relation)) {
			int index = Analyzer.translation.primaryRelations.indexOf(relation);
			analyzer.leafInfos.put(relation, new LeafInfo(relation, index));
		}
	}
	@Override
	public void visit(Variable variable) {
		if (Analyzer.translation.skolemRelations.containsKey(variable)) {
			Relation relation = Analyzer.translation.skolemRelations.get(variable);
			int index = Analyzer.translation.primaryRelations.indexOf(relation);
			analyzer.leafInfos.put(relation, new LeafInfo(relation, index));
		}
	}
}
